$\forall$${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), $A$:Type. Interface(${\it ds}$;${\it da}$;$A$) $\in$ Type